 {\em Higher-order process calculi} are calculi 
in which  processes  %(more generally, values containing processes)
can be communicated. 
They 
%Higher-order process calculi 
have been put forward in the 
early 1990s,
with 
 CHOCS \cite{Tho89} and Plain CHOCS
\cite{Tho93}, the  Higher-Order $\pi$-calculus 
\cite{San923}, and others. 
Higher-order (or process-passing) concurrency is often presented as an
alternative paradigm 
to the  first order (or name-passing) concurrency of the $\pi$-calculus
for the   description of   mobile systems.    
Higher-order calculi are formally closer to, and are inspired by, the
$\lambda$-calculus, whose basic computational step --- $\beta$-reduction ---
involves term instantiation. As in the $\lambda$-calculus, a computational step in higher-order calculi results in the
instantiation of a variable with a term, which is then
copied as many times as there are occurrences of the variable, resulting in potentially larger terms. 


%The basic  operators in higher-order calculi are usually those of
%CCS: parallel composition, input and output prefix, and restriction.
%Replication and recursion are often omitted as they can be encoded.

%Say something about recursion/replication.

%However, the  possibility of exchanging processes
% has  strong consequences on semantics: 
%ordinary definitions of bisimulation and behavioral equivalences
%become unsatisfactory, and   labeled transition systems must deal with
%higher-order substitutions and scope extrusion.


%The expressiveness of higher-order calculi has received little attention in the literature.
\hocore is a core calculus for higher-order concurrency, 
recently introduced in \cite{LanesePSS08}.
\hocore is \emph{minimal}, in that only the operators strictly necessary to obtain
 higher-order communications are retained. For instance,
continuations  following  output messages
   have been left out.  More importantly, \hocore has no restriction
   operator.
   Thus all channels are global, and
    dynamic creation of new channels is impossible.
    This makes
    the absence of recursion also relevant, as 
known encodings of fixed-point combinators in 
higher-order  process calculi
require the restriction
operator.
The grammar of \hocore processes is:
%We consider  a core calculus of Higher-Order processes (briefly
%\hocore), whose grammar is:
\[P :: = \inp a x. P \midd \Ho{a}{P} \midd P \parallel P \midd x \midd \nil \qquad \quad (*)\]  
An  input prefixed process 
$\inp a x . P$ can receive  on
name (or channel) $a$ a process that will be substituted in the place of $x$ in the body $P$;
an output message  $\Ho{a}{P}$ can send $P$ (the output object) on $a$;  parallel composition 
allows processes to interact. \hocore can be seen 
% We can  view the calculus 
as  a kind of concurrent
$\lambda$-calculus, where $\inp a x. P$ is a function, with formal
parameter $x$ and body $P$, located at  $a$; and
$\Ho{a}{P}$ is the argument  for a function located at $a$. 

Despite this minimality, via a termination preserving encoding of Minsky machines, \hocore was shown to be Turing complete. 
Therefore,  in \hocore, properties such as \emph{termination} (i.e. non existence of divergent computations) and 
\emph{convergence} (i.e. existence of a terminating computation) are both undecidable\footnote{Termination and convergence are also referred to as \emph{universal} and \emph{existential} termination, respectively.}. 
In contrast, somewhat surprisingly, strong bisimilarity is decidable. 
Furthermore, several sensible bisimilarities for higher-order calculus (including barb congruence) coincide with 
strong bisimilarity. 


In this paper, we shall aim at identifying the intrinsic source of expressive power in \hocore.
We shall focus on studying a restricted form of process output: the 
mentioned results for \hocore (in particular, the encoding of Minsky machines)
suggest that the capability of sending \emph{arbitrary} processes is intrinsically related to its expressive power. 
Therefore, investigating suitable limitations to the 
kind of processes that can be communicated in an output action seems a legitimate approach for assessing the source of the expressive power of higher-order concurrency.

To better understand our approach, let us consider the \hocore process below.
Intuitively, it receives a process on name $a$ and forwards it on name $b$ ($P_x$ stands for a process $P$ with free occurrences of variable $x$):
\[
R = a(x).\Ho{b}{P_x} 
\]
It is easy to see that since
objects in output actions are 
built following the syntax given by $(*)$, the actual structure of 
$P_x$ can be fairly complex. 
For instance, one could ``wrap'' the process to be received in $x$ using an arbitrary number of $k$ ``output layers'', i.e., to decree 
$P_x \equiv \Ho{b_1}{\Ho{b_2}{\ldots \Ho{b_k}{x}}\ldots}$. 
In our opinion, 
%We find 
this nesting capability 
%rather intriguing: not only it appears to be a somewhat artificial capability ---at least if one thinks of existing programming abstractions that consider code mobility--- but, more importantly, it 
embodies a great deal of the expressiveness of \hocore: as a matter of fact, the encoding of Minsky machines in \cite{LanesePSS08} depends critically on nesting-based counters.


%See where to put something like this:
With the above consideration in mind, in this paper we propose \ahopi, a sublanguage of \hocore in which output actions 
are limited so to rule out such a nesting capability. In \ahopi, 
%have the following limitation: 
every output object must be structurally congruent to the parallel composition of two kinds of processes: 
(i) a number of processes received from other processes (possibly open), and 
(ii) a number of closed processes that available in the local context of the sender. 
Hence, the context in which the output action resides can only
contribute to communication by ``appending'' pieces of code that are available in the form of a black-box.
More formally, 
%it would be interesting to see what happens if the forwarding capabilitties are restricted to a parallel composition of a number of copies of the received process, along with a number of arbitrary --yet closed-- processes.
%That is, 
the grammar of \ahopi processes is that in $(*)$, excepting the production for output actions, which 
is replaced by the following one:
%a syntax where the grammar for output is replaced by
\[
\Ho{a}{ x_1 \parallel \cdots \parallel x_k \parallel P}
\]
where $k \geq 0$ and $P$ is a closed process.
This modification 
directly restricts
forwarding capabilities for output processes, which in turn, leads to a more limited structure of processes along reductions.

%We call \emph{threads} this kind of restricted processes that can appear in output position.

In addition to the above motivations related to expressiveness, 
the limited style of higher-order communication enforced in \ahopi turns out to be interesting from a more pragmatic standpoint.
%there are pragmatic reasons for considering this limited 
%style of higher-order communication.
In fact, communication in \ahopi 
is inspired by those cases in which a process $P$
is communicated in a translated format $\encp{P}{}$,
and the translation is not compositional. That is, the cases in which, 
for any  process context $C$, 
the translation of $\ct{P}$ cannot be seen as a function of
the translation of $P$, i.e. $\encp{ \ct{P}}{} \neq \encp{ C}{}[\encp{P}{}]$.
%This happens in many cases, e.g. already compiled code,
%obfuscated code, proof carrying code.
%This reasoning on the theoretical side is intimately related with the pragmatic motivations for studying limited forms of forwading. In fact, thread communication reminds us of several practical scenarios of mobile code. For instance. one could think of it of the case where mobile code is closed in the sense that the recipient cannot ``examine'' the code and it is only allowed to executed, possibily in cooperation of a local contexts, here represented by the closed processes. 
This abstract setting can be related to existing programming scenarios. 
The simplest example is perhaps mobility based on already compiled code.
Other examples include \emph{proof-carrying code} \cite{NeculaL98}, in which the code that is mobile is both executable and certified, and cannot be modified by a recipient; and communication of \emph{obfuscated code} \cite{CollbergT02}, i.e. source code that is made difficult to understand for, e.g., security/copyright reasons, while preserving its functionality.

The main contribution of the paper is the study of the expressiveness and decidability of termination and convergence in \ahopi.
%This paper then deals with the expressiveness of core higher-order calculi in which process communicated is replaced with this form of thread communication, 
Our main results are:
%We shall concentrate on the expressive power of this fragment of HOcore and on the decidability of termination. Accordingly, the major results of the present paper are
\begin{enumerate}
\item Similarly as \hocore, \ahopi is Turing complete. Therefore, despite the limitation of forward capabilities motivated above, the calculus has a significant expressive power. Consequently, convergence in \ahopi is undecidable.
This result is obtained by exhibiting a non-deterministic encoding of Minsky machines. 
%; unlike the encoding in LICS, however, the presented encoding is non-deterministic, and as such, it offers a weaker encodability guarantee. 

\item In sharp contrast with \hocore, termination in \ahopi is decidable. 
This result is obtained by appealing to the theory of well-structured transition systems (WSTS) \cite{FinkelS01}, following the proof strategy used in \cite{Busi09}.
\end{enumerate}

As for (1) it is worth commenting that since the presented encoding is non deterministic, it offers \emph{weaker} guarantees for encodability of Minsky machines. These weaker guarantees shall be discussed at the end of the paper. As for (2), although using the theory of WSTS is certainly not a new approach, to the best of our knowledge this is the first time it is applied in the higher-order case. This is significant because
its adaptation to the \ahopi case is far from trivial. Indeed, as we shall discuss, the approach based in WSTS relies on over-approximating a bound on the (set of) derivatives of a process.
Even with the limitation on forwarding, because of the ``term copying'' feature of higher-order calculi, finding suitable ways of ``bounding'' such a set is rather challenging. 
